A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} , k:{k:Knd| (k  fpf-domain(I(i).2))} .
(I(i).2(k).2)  State(I(i).1)(I(i).2(k).1)(A + Top) 

latex

Definitions

x:A. B(x), t  T, t.2, f(x), x. t(x), P  Q, t.1, a:A fp B(a), S  T, , Knd, Top, MaInterface(T), fpf-domain(f), x(s), P  Q, P  Q, P & Q

Lemmas

Knd wf, l member wf, fpf-domain wf, Id wf, ma-interface wf, fpf wf, assert wf, hasloc wf, decl-state wf, top wf, pi2 wf, pi1 wf, fpf-ap wf, Kind-deq wf, l member-subtype rel, decidable assert, decidable equal Kind, contravariance-variant, member-fpf-domain, ma-interface-da-type2, ma-interface-type-trivial, fpf-dom wf, subtype rel product, subtype rel list, IdLnk wf, subtype rel set, subtype rel function, subtype-set-hasloc